Nuprl Definition : w-kindtype 0,22

w-kindtype(TA;M;i)(k)
== kindcase(ka.TA(a); l,tg.if destination(l) = i M(l,tg) else Void fi ) 
latex


Definitionsx.A(x), kindcase(ka.f(a); l,t.g(l;t) ), if b t else f fi, a = b, destination(l), f(a), Void
FDL editor aliasesw-kindtype

origin